Nuprl Lemma : d-decl_wf
0,22
postcript
pdf
D
:Dsys,
i
:Id. d-decl(
D
;
i
)
Knd
Type
latex
Definitions
d-decl(
D
;
i
)
,
w-action-dec(
TA
;
M
;
i
)
,
M
.da(
a
)
,
locl(
a
)
,
M
.dout(
l
,
tg
)
,
M(
i
)
,
source(
l
)
,
x
:
A
.
B
(
x
)
,
IdLnk
,
Id
,
t
T
,
Dsys
Lemmas
dsys
wf
,
Id
wf
,
IdLnk
wf
,
lsrc
wf
,
d-m
wf
,
ma-dout
wf
,
locl
wf
,
ma-da
wf
,
w-action-dec
wf
origin
D:Dsys, i:Id. d-decl(D;i) 
Knd
Type D:Dsys, i:Id. d-decl(D;i) KndType x:A. B(x) T